In designing large dynamic systems such as, for example, a complex electronic circuit, the design is often analyzed to verify a selected property. For example, the design may need to be analyzed to verify that the system does not enter a certain failed or erroneous state under any normal set of inputs to the system in any finite number of steps (e.g., a safety property).
Several Boolean satisfiability solvers (also referred to as SAT solvers) are known that can determine whether the system may enter a given failed state within a selected number of steps. Typically, the Boolean SAT solver searches for a counterexample to a given safety property. A counterexample is a sequence of input values to the system that will cause the system to enter the failed state within the selected number of steps.
If the Boolean SAT solver finds a counterexample within K steps, the counterexample indicates an error in the design, and can aid the designer in redesigning the system to ensure that the failed state is not entered. If the Boolean SAT solver finds that there is no counterexample within K steps, the designer's confidence in the correctness of the design is increased.
Boolean SAT solvers require a model of a design to be represented as Boolean operatives such as NAND, NOR, AND, OR, and NOT functions with Boolean variables. At such a low level description, extensive computing resources may be needed to perform verification of a complex design. Moreover, the time to perform verification of a complex design may be lengthy. Thus, it is desirable to improve upon Boolean SAT solvers for the purpose of design verification.